A:Type, B:(AType), f:x:A fp B(x), C:Type, a:(A(C+Unit)), b:(CA).
(y:A. isl(a(y))  b(outl(a(y))) = y)  compose-fpf(a;b;f)  y:C fp B(b(y)) 

latex

Definitions	t  T, x:A. B(x), (x  l), A & B, Unit, isl(x), P & Q, x:A. B(x), b, True, T, P  Q, SqStable(P), , outl(x), P  Q, mapfilter(f;P;L), f o g, fpf-domain(f), a:A fp B(a), 2of(t), x(s), compose-fpf(a;b;f), x. t(x), Prop
Lemmas	squash wf, true wf, fpf wf, mapfilter wf, member map filter, outl wf, sq stable from decidable, decidable assert, assert wf, isl wf, unit wf, l member wf